Nuprl Lemma : ma-interface-consistent-at-compose 11,40
A, B:Type, g:(A(B + Top)), X:MaInterface(A), es:ES, i:Id.
(i  dom(X))
 (ma-interface-consistent-at(es;i;X)
  ma-interface-consistent-at(es;i;ma-interface-compose(g;X))) 
latex

Definitionsx:A. B(x), P  Q, P  Q, ma-interface-consistent-at(es;i;X), ma-interface-compose(g;X), P & Q, t  T, x. t(x), , P  Q, t.1, MaInterface(T), x(s)
Lemmasfpf-ap wf, id-deq wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, fpf-dom wf, Kind-deq wf, strong-subtype-deq-subtype, strong-subtype-set3, strong-subtype-self, fpf-trivial-subtype-top, alle-at wf, es-kind wf, subtype rel wf, es-valtype wf, pi1 wf, es-E wf, es-loc wf, es-vartype wf, fpf-cap wf, Id wf, event system wf, ma-interface wf

origin